Tute - Completed (Week 1)
Table of Contents
1. Predicate Logic
1.1. Question 1
For which values of \(A\) and \(B\) does the boolean expression \(\varphi = \neg (A \Rightarrow B) \lor \neg B\) hold?
Using a truth table:
\(A\) | \(B\) | \(A \Rightarrow B\) | \(\neg B\) | \(\varphi\) |
\(\bot\) | \(\bot\) | \(\top\) | \(\top\) | \(\top\) |
\(\bot\) | \(\top\) | \(\top\) | \(\bot\) | \(\bot\) |
\(\top\) | \(\bot\) | \(\bot\) | \(\top\) | \(\top\) |
\(\top\) | \(\top\) | \(\top\) | \(\bot\) | \(\bot\) |
This is an answer but it is not so informative. Using boolean algebra manipulation instead:
\begin{array}{lcl} \neg (A \Rightarrow B) \lor \neg B & = & \neg (\neg A \lor B) \lor \neg B \\ & = & (A \land \neg B) \lor \neg B \\ & = & (A \lor \neg B) \land (\neg B \lor \neg B) \\ & = & (A \lor \neg B) \land \neg B \\ & = & \neg B \\ \end{array}Here we can see clearly that \(\varphi\) holds only when \(B\) is false, and the value of \(A\) does not matter.
1.2. Question 2
Simplify the boolean expression \((A \Rightarrow B) \lor (B \Rightarrow A)\)
This proof is not constructive. Discuss what it means for a proof to be constructive.
1.3. Question 3
A binary connective \(\bullet\) is defined as follows:
\(A\) | \(B\) | \(A\ \bullet\ B\) |
\(\bot\) | \(\bot\) | \(\top\) |
\(\bot\) | \(\top\) | \(\bot\) |
\(\top\) | \(\bot\) | \(\top\) |
\(\top\) | \(\top\) | \(\top\) |
Restate the formula \(A \lor B\) in terms of \(\bullet\). What is the \(\bullet\) connective?
\(A \bullet \neg B\), \(\bullet\) is a flipped implication operator. The ex falso quodlibet principle is relevant here: from false, you can prove anything.
1.4. Question 4
Assuming that \(F(x)\) states that the person \(x\) is my friend and that \(P(x)\) states that the person \(x\) is perfect, what is a logical translation of the phrase "None of my friends are perfect"?
One option is \(\lnot \exists x. \; F(x) \land P(x)\), which can be read literally as saying "there does not exist a person \(x\) such that they are both my friend and perfect" in plain English. There are a number of other equally-valid translations too:
- \(\forall x. \; F(x) \Rightarrow \lnot P(x)\), which can be read as saying "if a person is my friend, then they aren't perfect".
- \(\forall x. \; P(x) \Rightarrow \lnot F(x)\), which can be read as saying "if a person is perfect, then they aren't my friend".
The logical formulae for all 3 are equivalent. As an exercise, prove this!
1.5. Question 5
Given the following function
\[ f (n) = \begin{cases} 0 & \text{if}\ n = 0 \\ 2n - 1 + f(n-1) & \text{if}\ n > 0 \end{cases} \]
Prove that \(\forall n \in \mathbb{N}.\ f(n) = n^2\).
Proof by mathematical induction on the natural number \(n\).
Base Case: \(n = 0\)
\begin{array}{lcl} f(0) & = & 0 \\ & = & 0^2 \\ & & \blacksquare \end{array}Inductive Case: \(n = k + 1\), for arbitrary \(k \in \mathbb{N}\). Assume the inductive hypothesis that \(f(k) = k^2\).
\begin{array}{lcl} f(k+1) & = & 2(k+1) - 1 + f(k) \\ & = & 2k + 2 - 1 + f(k) \\ & = & 2k + 1 + f(k) \\ & = & 2k + 1 + k^2 \quad \text{(I.H)}\\ & = & k^2+k+k+1 \\ & = & k(k+1)+(k+1) \\ & = & (k+1)(k+1) \\ & = & (k+1)^2 \\ & & \blacksquare \end{array}Thus \(f(n) = n^2\) for all \(n \in \mathbb{N}\).
2. Haskell
Consider the Haskell code written in the lecture.
2.1. Haskell lexical structure
- What is the difference between a
data
and atype
declaration? - What is the difference between a type and a data constructor? List the identifiers in the code which represent type names, and those which represent data constructor names.
- Which phase of the compiler would be responsible for distinguishing type and data constructors?
1: A data
declaration introduces a new type, for example the Tree
type below.
type
keyword just introduces a new name for an existing type, like typedef
in C.
For example, the String
type in the standard library is defined merely to be [Char]
using a type
declaration.
2: A data constructor describes a way to create a value of a certain type. For example,
the data constructors in the below Tree
type are Leaf
and Branch
:
data Tree a = Branch a (Tree a) (Tree a) | Leaf
3: The parser is responsible, as it requires information from the grammar of the language
to determine if, for example, Tree
is a data constructor or a type name, as it is
lexically indistinguishable.
2.2. Haskell programming
Write a Haskell function
mySum
that sums all elements in a list of numbers. Feel free to use the following template:mySum :: [Int] -> Int mySum [] = ??? mySum (n:ns) = ???
- Write a Haskell function
myProduct
that multiplies all elements in a list of numbers. You probably used copypaste to solve the previous question, didn't you? No reason to be ashamed, we've all done it! But let's try not to.
Find a generalisation
myBinop
that applies a given binary operatorf
with unit elementz
to a list of numbers. We will then be able to definemyProduct
andmySum
usingmyBinop
.myBinop :: (Int -> Int -> Int) -> Int -> ([Int] -> Int) myBinop f z [] = ??? myBinop f z (n:ns) = ??? mySum :: [Int] -> Int mySum ns = myBinop (+) 0 ns myProduct :: [Int] -> Int myProduct ns = myBinop (*) 1 ns
We just reinvented a wheel. The fold functions are general-purpose library functions that completely subsume
myBinop
. Try to implementmySum
andmyProduct
usingfoldr
instead ofmyBinop
.The linked library documentation references a lot of concepts that we don't assume familiarity with, so don't worry if you don't fully understand it. Perhaps start by looking at the examples.
mySum :: [Int] -> Int mySum [] = 0 mySum (n:ns) = n + mySum ns myProduct :: [Int] -> Int myProduct [] = 1 myProduct (n:ns) = n*myProduct ns myBinop :: (Int -> Int -> Int) -> Int -> ([Int] -> Int) myBinop f z [] = z myBinop f z (n:ns) = n `f` myBinop f z ns mySum2 :: [Int] -> Int mySum2 = myBinop (+) 0 myProduct2 :: [Int] -> Int myProduct2 = myBinop (*) 1 mySum3 :: [Int] -> Int mySum3 = foldr (+) 0 myProduct3 :: [Int] -> Int myProduct3 = foldr (*) 1
3. Subtyping Sins
The Monday lecture demonstrated a flaw in Java's static type system. It's been there for decades and it's well-known, including by the Java developers. Yet they've chosen not to fix it. Why do you think that is?
There's no right or wrong answer to this question (unless your name is James Gosling).